$\forall$$E$, $X_{1}$, $X_{2}$:Type, ${\it info}$:($E$$\rightarrow$(Id$\times$$X_{1}$+(IdLnk$\times$$E$)$\times$$X_{2}$)), ${\it pred?}$:($E$$\rightarrow$($E$+Unit)), $e$, ${\it e'}$:$E$.
\\[0ex]pred!($e$;${\it e'}$) $\in$ Prop